{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators,
  UndecidableInstances, ScopedTypeVariables, MultiParamTypeClasses,
  FlexibleInstances #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module CnvExample2 (Cnv, Convert) where

import TypeBasics
import Yoko



data Exp = Const Int | Plus Exp Exp



data Fds_Const = Fds_Const Int
data Fds_Plus  = Fds_Plus  Exp Exp
type instance Tag Fds_Const = TagConst   ;   data TagConst
type instance Tag Fds_Plus  = TagPlus    ;   data TagPlus
type instance Range Fds_Const = Exp
type instance Range Fds_Plus  = Exp
instance DC Fds_Const where rejoin (Fds_Const i)     = Const i
instance DC Fds_Plus  where rejoin (Fds_Plus  el er) = Plus  el er
type instance DCs Exp = N Fds_Const :+: N Fds_Plus
instance DT Exp where
  disband (Const i)     = DCsOf $ L . N $ Fds_Const  i
  disband (Plus  el er) = DCsOf $ R . N $ Fds_Plus   el er
type instance Rep Fds_Const = Dep Int
type instance Rep Fds_Plus  = Rec Exp :*: Rec Exp
instance Generic Fds_Const where
  rep ~(Fds_Const i) = Dep i
  obj ~(Dep i)         = Fds_Const i
instance Generic Fds_Plus where
  rep ~(Fds_Plus el er) = Rec el :*: Rec er
  obj ~(Rec el :*: Rec er) = Fds_Plus el er





data Exp2 = Const2 Int (Maybe Exp2) | Plus2 Exp2 Exp2 deriving Show



data Fds_Const2 = Fds_Const2 Int (Maybe Exp2)
data Fds_Plus2  = Fds_Plus2  Exp2 Exp2
type instance Tag Fds_Const2 = TagConst2   ;   data TagConst2
type instance Tag Fds_Plus2  = TagPlus2    ;   data TagPlus2
type instance Range Fds_Const2 = Exp2
type instance Range Fds_Plus2  = Exp2
instance DC Fds_Const2 where rejoin (Fds_Const2 i me)     = Const2 i me
instance DC Fds_Plus2  where rejoin (Fds_Plus2  el er) = Plus2  el er
type instance DCs Exp2 = N Fds_Const2 :+: N Fds_Plus2
instance DT Exp2 where
  disband (Const2 i me)  = DCsOf $ L . N $ Fds_Const2 i me
  disband (Plus2  el er) = DCsOf $ R . N $ Fds_Plus2  el er
type instance Rep Fds_Const2 = Dep Int :*: Maybe (Rec Exp2)
type instance Rep Fds_Plus2  = Rec Exp2 :*: Rec Exp2
instance Generic Fds_Const2 where
  rep ~(Fds_Const2 i me) = Dep i :*: fmap Rec me
  obj ~(Dep i :*: me)       = Fds_Const2 i (fmap unRec me)
instance Generic Fds_Plus2 where
  rep ~(Fds_Plus2 el er) = Rec el :*: Rec er
  obj ~(Rec el :*: Rec er) = Fds_Plus2 el er











type instance IsPrefixOf TagConst TagConst2 = True
type instance IsPrefixOf TagConst TagPlus2  = False
type instance IsPrefixOf TagPlus  TagConst2 = False
type instance IsPrefixOf TagPlus  TagPlus2  = True









type instance Cnv cnv (DCsOf t sum) = Cnv cnv t
instance ConvertSumTo cnv sum (Cnv cnv t) => Convert cnv (DCsOf t sum) where
  convert cnv = convertSumTo cnv . unDCsOf




type family Cnv cnv a
class Convert cnv a where convert :: cnv -> a -> Cnv cnv a

data ToExp2 = ToExp2
type instance Cnv ToExp2 Exp = Exp2

instance Convert ToExp2 Exp where
  convert cnv e = case project (disband e) of
    Left  (Fds_Const i) -> Const2 i Nothing
    Right x             -> convert cnv x

{- ill-typed:     "Couldn't match type `Maybe (Rec Exp2)' with `Int'"
              and "Couldn't match type `(:*:) (Dep Int)' with `D'"
              because the fields of Const and Const2 are inequal
   convert = convert . disband -}




class ConvertSumTo cnv sum t where convertSumTo :: cnv -> sum -> t

instance (ConvertSumTo cnv a t, ConvertSumTo cnv b t
         ) => ConvertSumTo cnv (a :+: b) t where
  convertSumTo cnv = foldPlus (convertSumTo cnv) (convertSumTo cnv)

-- NB only works if there's exactly one matching constructor
instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),
          ConvertRs cnv (Rep dc), Rep dc' ~ RsConvert cnv (Rep dc),
          DC dc', Range dc' ~ t, DT t
         ) => ConvertSumTo cnv (N dc) t where
  convertSumTo cnv =
    foldN $ rejoin . (id :: dc' -> dc') . obj . convertRs2 cnv . rep



type family FindDCs s sum
type instance FindDCs s (N dc) =
  If (IsPrefixOf s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)




-- applies cnv to every Rec in a product; identity on other factors
type family RsConvert cnv prod
class ConvertRs cnv prod where convertRs2 :: cnv -> prod -> RsConvert cnv prod

type instance RsConvert cnv (Rec a) = Rec (Cnv cnv a)
instance Convert cnv a => ConvertRs cnv (Rec a) where
  convertRs2 cnv (Rec x) = Rec (convert cnv x)

type instance RsConvert cnv (Dep a) = Dep a
type instance RsConvert cnv U     = U
instance ConvertRs cnv (Dep a) where convertRs2 _ = id
instance ConvertRs cnv U     where convertRs2 _ = id

type instance RsConvert cnv (a :*: b) = RsConvert cnv a :*: RsConvert cnv b
instance (ConvertRs cnv a, ConvertRs cnv b) => ConvertRs cnv (a :*: b) where
  convertRs2 cnv = mapTimes (convertRs2 cnv) (convertRs2 cnv)



ex0 = convert ToExp2 (Plus (Const 3) (Const 4))




concat `fmap` mapM derive [''Fds_Const, ''Fds_Plus, ''Exp,
                           ''Fds_Const2, ''Fds_Plus2, ''Exp2]
